ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), upd:update-spec(ds; da).
update-spec-decl(upd; ds)  prop{i:l} 

latex

Definitions	Id, t  T, Type, x. t(x), x:A. B(x), fpf(A; a.B(a)), Knd, update-spec(ds; da), x.A(x), top, x:AB(x), id-deq, fpf-dom(eq; x; f), b, prop{i:l}, update-spec-vars(upd), (x  l), P  Q, update-spec-decl(upd; ds)
Lemmas	l member wf, update-spec-vars wf, assert wf, fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, update-spec wf, Knd wf, fpf wf, Id wf